A:Type, d:EqDecider(A), i,j:A. (i = j)  sqequal((eqof(d)(i,j)); tt) 

latex

Definitions	x:A. B(x), P  Q, eqof(d), t  T, t.1, prop{i:l}, EqDecider(T), sq_type(T), guard(T), , P  Q, P  Q, Unit, A, False, tt, , ff
Lemmas	bool sq, deq wf, bool wf, eqtt to assert, btrue wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot